$\vdash$  $\forall$$A$, $B$:Type, $f$:($A$$\rightarrow$($B$ + Top)). $f$ o p{-}id()   = $f$